es-x-equiv(es; i; x; s1; s2) == z:Id. ((z = x))  (s1(z) = s2(z)) 

latex

---

clarification:

es-x-equiv(es; i; x; s1; s2)
== z:Id. ((z = x  Id))  (s1(z) = s2(z)  es_vartype(es; i; z)) 

latex

Definitions	x:A. B(x), P  Q, A, Id, s = t, es_vartype(es; i; x), f(a)
FDL editor aliases	es-x-equiv